package platform.service.inv;

import com.alibaba.fastjson.JSONArray;
import com.alibaba.fastjson.JSONObject;
import common.struct.ConstantEnum.CheckResult;
import common.util.Util;
import daikon.Daikon;
import daikon.inv.Invariant;
import daikon.inv.OutputFormat;

import java.io.*;
import java.util.*;

public class InvGroup {
    public List<InvData> datas;

    public final double[] centroid;
    public double radius;
    public List<Inv> invs = null;

    public int passed = 0;
    public int violated = 0;

    public String appName;
    public int lineId;
    public int grpId;

    public Object simpleToJSON() {
        if (invs == null) {
            return null;
        }
        JSONObject ret = new JSONObject();
        ret.put("passed", passed);
        ret.put("violated", violated);
        JSONArray arr = new JSONArray();
        for (Inv inv : invs) {
            arr.add(inv.toString());
        }
        ret.put("invs", arr);
        return ret;
    }

    public Object fullToJSON() {
        if (invs == null) {
            return null;
        }
        JSONObject ret = new JSONObject();

        JSONArray dataArr = new JSONArray();
        for (InvData data : datas) {
            dataArr.add(data.toJSON());
        }
        ret.put("datas", dataArr);

        JSONArray centroidArr = new JSONArray();
        for (double v : centroid) {
            centroidArr.add(v);
        }
        ret.put("centroid", centroidArr);
        ret.put("radius", radius);
        JSONArray arr = new JSONArray();
        for (Inv inv : invs) {
            arr.add(inv.toString());
        }
        ret.put("invs", arr);

        ret.put("passed", passed);
        ret.put("violated", violated);

        ret.put("app_name", appName);
        ret.put("line_id", lineId);
        ret.put("grp_id", grpId);

        return ret;
    }

    public static InvGroup fromJSON(JSONObject jo) {
        JSONArray centroidArr = jo.getJSONArray("centroid");
        InvGroup ret = new InvGroup(centroidArr.size(),
                jo.getString("app_name"),
                jo.getIntValue("line_id"),
                jo.getIntValue("grp_id"));
        JSONArray dataArr = jo.getJSONArray("datas");
        List<InvData> invDatas = new ArrayList<>();
        for (int i = 0; i < dataArr.size(); i++) {
            invDatas.add(InvData.fromJSON(dataArr.getJSONObject(i)));
        }
        ret.datas.addAll(invDatas);
        for (int i = 0; i < centroidArr.size(); i++) {
            ret.centroid[i] = centroidArr.getDouble(i);
        }
        ret.radius = jo.getDoubleValue("radius");
        JSONArray invArr = jo.getJSONArray("invs");
        ret.invs = new ArrayList<>();
        for (int i = 0; i < invArr.size(); i++) {
            ret.invs.add(new Inv(invArr.getString(i)));
        }
//        ret.passed = jo.getIntValue("passed");
//        ret.violated = jo.getIntValue("violated");
        return ret;
    }

    @Override
    public String toString() {
        return simpleToJSON().toString();
    }

    public InvGroup(int len, String appName, int lineId, int grpId) {
        datas = new ArrayList<>();
        centroid = new double[len];

        this.appName = appName;
        this.lineId = lineId;
        this.grpId = grpId;
    }

    public CheckResult check(InvData data) {
        CheckResult ret = CheckResult.INV_PASSED;
        for (Inv inv : invs) {
            Map<String, Object> checkVals = new HashMap<>(data.checkVals);
            if (!inv.check(checkVals)) {
                ret = CheckResult.INV_VIOLATED;
                break;
            }
//            if (inv instanceof daikon.inv.unary.UnaryInvariant) {
//                UnaryInvariant inv1 = (UnaryInvariant) inv;
//                if (inv1.check(data.checkVals.get(inv1.ppt.var_infos[0].name()), 1, 1) != InvariantStatus.NO_CHANGE) {
//                    ret = CheckResult.INV_VIOLATED;
//                    break;
//                }
//            } else if (inv instanceof daikon.inv.binary.BinaryInvariant) {
//                BinaryInvariant inv2 = (BinaryInvariant) inv;
//                if (inv2.check(data.checkVals.get(inv2.ppt.var_infos[0].name()),
//                        data.checkVals.get(inv2.ppt.var_infos[1].name()), 1, 1) != InvariantStatus.NO_CHANGE) {
//                    ret = CheckResult.INV_VIOLATED;
//                    break;
//                }
//            } else if (inv instanceof daikon.inv.ternary.TernaryInvariant) {
//                TernaryInvariant inv3 = (TernaryInvariant) inv;
//                if (inv3.check(data.checkVals.get(inv3.ppt.var_infos[0].name()),
//                        data.checkVals.get(inv3.ppt.var_infos[1].name()),
//                        data.checkVals.get(inv3.ppt.var_infos[2].name()), 1, 1) != InvariantStatus.NO_CHANGE) {
//                    ret = CheckResult.INV_VIOLATED;
//                    break;
//                }
//            }
        }
        if (ret == CheckResult.INV_PASSED) {
            passed++;
        } else {
            violated++;
        }
        return ret;
    }

    public void invGen() {
        //TODO
        File dir = new File("output/platform/inv/" + appName + "/line" + lineId);
        if (!dir.exists()) {
            dir.mkdirs();
        }

        //trace output
        String declsFileName = dir.getAbsolutePath() + "/grp" + grpId + ".decls";
        File declFile = new File(declsFileName);
        if (!declFile.exists()) {
            BufferedWriter out = null;
            try {
                out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(declFile, true)));
                out.write("DECLARE\n" + appName + "-" + lineId + "-" + grpId + ":::POINT\n");
                for (Map.Entry<String, Double> entry : datas.get(0).checkVals.entrySet()) {
                    String k = entry.getKey();
                    try {
                        out.write(k + "\ndouble\ndouble\n1\n");
                    } catch (IOException e) {
                        e.printStackTrace();
                    }
                }
                out.close();
            } catch (IOException e) {
                throw new RuntimeException(e);
            }
        }
        String varFileName = dir.getAbsolutePath() + "/grp" + grpId + ".dtrace";
        File varFile = new File(varFileName);
        if (!varFile.exists()) {
            BufferedWriter out = null;
            try {
                String title = appName + "-" + lineId + "-" + grpId + ":::POINT\n";
                out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(varFile, true)));
                for (InvData data : datas) {
                    out.write(title);
                    for (Map.Entry<String, Double> entry : data.checkVals.entrySet()) {
                        String k = entry.getKey();
                        Double v = entry.getValue();
                        try {
                            out.write(k + "\n" + v + "\n1\n");
                        } catch (IOException e) {
                            e.printStackTrace();
                        }
                    }
                    out.write("\n");
                }
                out.close();
            } catch (IOException e) {
                throw new RuntimeException(e);
            }
        }
        String invGzFileName = dir.getAbsolutePath() + "/grp" + grpId + ".inv.gz";

        //inv gen
        String[] daikonArgs = new String[] {
                varFileName,
                declsFileName,
//                "--no_text_output",
                "-o",
                invGzFileName,
                "--config",
                "Resources/config/platform/inv/config.txt",
        };
        PlatformInvServer.lockDaikon();
        daikon.Daikon.main(daikonArgs);
        List<Invariant> invs = Daikon.all_ppts.get(appName + "-" + lineId + "-" + grpId + ":::POINT").getInvariants();
        this.invs = new ArrayList<>();
        for (Invariant inv : invs) {
            this.invs.add(new Inv(inv.format_using(OutputFormat.JAVA)));
        }
//        for (Invariant inv : invs) {
//            PlatformInvServer.invCaches.put(inv.format(), inv);
//        }
        PlatformInvServer.unlockDaikon();

        //inv output
        String invFileName = dir.getAbsolutePath() + "/grp" + grpId + ".inv";
        File invFile = new File(invFileName);
        if (!invFile.exists()) {
            BufferedWriter out = null;
            try {
                out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(invFile, true)));
                out.write("invariant,type,samples,confidence\n");
                for (Invariant inv : invs) {
                    out.write(inv.format() +
                            "," +
                            inv.getClass().getName() +
                            "," +
                            inv.ppt.num_samples() +
                            "," +
                            inv.getConfidence() +
                            "\n");
                }
                out.close();
            } catch (IOException e) {
                throw new RuntimeException(e);
            }
        }
    }

    public static InvGroup makeGroup(String appName, int lineId, int grpId, InvData... datas) {
        int len = datas[0].envCtxVals.length;
        InvGroup ret = new InvGroup(len, appName, lineId, grpId);
        ret.datas.addAll(Arrays.asList(datas));
        for (InvData data : datas) {
            for (int i = 0; i < len; i++) {
                ret.centroid[i] += data.envCtxVals[i];
            }
        }
        for (int i = 0; i < len; i++) {
            ret.centroid[i] /= datas.length;
        }
        double maxDist = 0;
        for (InvData data : datas) {
            double dist = Util.distance(ret.centroid, data.envCtxVals);
            if (dist > maxDist) {
                maxDist = dist;
            }
        }
        ret.radius = maxDist;
        return ret;
    }

    public void add(InvData... newDatas) {
        int oldSize = datas.size();
        datas.addAll(Arrays.asList(newDatas));
        for (int i = 0; i < centroid.length; i++) {
            centroid[i] = centroid[i] * oldSize;
        }
        for (InvData data : newDatas) {
            for (int i = 0; i < centroid.length; i++) {
                centroid[i] += data.envCtxVals[i];
            }
        }
        for (int i = 0; i < centroid.length; i++) {
            centroid[i] /= datas.size();
        }
        double maxDist = 0;
        for (InvData data : datas) {
            double dist = Util.distance(centroid, data.envCtxVals);
            if (dist > maxDist) {
                maxDist = dist;
            }
        }
        radius = maxDist;
    }

    public int size() {
        return datas.size();
    }
}
